(set-info :smt-lib-version 2.6)
(set-logic UF)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011.  Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :category "industrial")
(set-info :status sat)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-sort S3 0)
(declare-sort S4 0)
(declare-sort S5 0)
(declare-sort S6 0)
(declare-sort S7 0)
(declare-sort S8 0)
(declare-sort S9 0)
(declare-sort S10 0)
(declare-sort S11 0)
(declare-sort S12 0)
(declare-sort S13 0)
(declare-sort S14 0)
(declare-sort S15 0)
(declare-sort S16 0)
(declare-sort S17 0)
(declare-sort S18 0)
(declare-sort S19 0)
(declare-sort S20 0)
(declare-sort S21 0)
(declare-sort S22 0)
(declare-sort S23 0)
(declare-sort S24 0)
(declare-sort S25 0)
(declare-sort S26 0)
(declare-sort S27 0)
(declare-sort S28 0)
(declare-sort S29 0)
(declare-sort S30 0)
(declare-sort S31 0)
(declare-sort S32 0)
(declare-sort S33 0)
(declare-sort S34 0)
(declare-sort S35 0)
(declare-sort S36 0)
(declare-sort S37 0)
(declare-sort S38 0)
(declare-sort S39 0)
(declare-sort S40 0)
(declare-sort S41 0)
(declare-sort S42 0)
(declare-sort S43 0)
(declare-sort S44 0)
(declare-sort S45 0)
(declare-sort S46 0)
(declare-sort S47 0)
(declare-sort S48 0)
(declare-sort S49 0)
(declare-sort S50 0)
(declare-sort S51 0)
(declare-sort S52 0)
(declare-sort S53 0)
(declare-sort S54 0)
(declare-sort S55 0)
(declare-sort S56 0)
(declare-sort S57 0)
(declare-sort S58 0)
(declare-sort S59 0)
(declare-sort S60 0)
(declare-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (S2 S3) S3)
(declare-fun f4 (S4 S5) S2)
(declare-fun f5 () S4)
(declare-fun f6 () S5)
(declare-fun f7 () S3)
(declare-fun f8 () S3)
(declare-fun f9 () S5)
(declare-fun f10 () S5)
(declare-fun f11 () S5)
(declare-fun f12 () S5)
(declare-fun f13 () S3)
(declare-fun f14 () S5)
(declare-fun f15 (S7 S6) S6)
(declare-fun f16 (S8 S9) S7)
(declare-fun f17 () S8)
(declare-fun f18 () S9)
(declare-fun f19 () S6)
(declare-fun f20 (S10 S5) S5)
(declare-fun f21 (S11 S12) S10)
(declare-fun f22 () S11)
(declare-fun f23 () S12)
(declare-fun f24 (S14 S13) S13)
(declare-fun f25 (S15 S16) S14)
(declare-fun f26 () S15)
(declare-fun f27 () S16)
(declare-fun f28 () S13)
(declare-fun f29 (S18 S17) S17)
(declare-fun f30 (S19 S20) S18)
(declare-fun f31 () S19)
(declare-fun f32 () S20)
(declare-fun f33 () S17)
(declare-fun f34 (S22 S21) S21)
(declare-fun f35 (S23 S24) S22)
(declare-fun f36 () S23)
(declare-fun f37 () S24)
(declare-fun f38 () S21)
(declare-fun f39 (S26 S25) S25)
(declare-fun f40 (S27 S28) S26)
(declare-fun f41 () S27)
(declare-fun f42 () S28)
(declare-fun f43 () S25)
(declare-fun f44 (S29 S9) S9)
(declare-fun f45 (S30 S25) S29)
(declare-fun f46 () S30)
(declare-fun f47 (S31 S16) S16)
(declare-fun f48 (S32 S21) S31)
(declare-fun f49 () S32)
(declare-fun f50 (S33 S12) S12)
(declare-fun f51 (S34 S17) S33)
(declare-fun f52 () S34)
(declare-fun f53 (S2) S1)
(declare-fun f54 (S35 S5) S6)
(declare-fun f55 () S35)
(declare-fun f56 () S6)
(declare-fun f57 (S36 S3) S35)
(declare-fun f58 () S36)
(declare-fun f59 (S37 S12) S6)
(declare-fun f60 (S38 S5) S37)
(declare-fun f61 () S38)
(declare-fun f62 (S39 S16) S6)
(declare-fun f63 (S40 S13) S39)
(declare-fun f64 () S40)
(declare-fun f65 (S41 S20) S6)
(declare-fun f66 (S42 S17) S41)
(declare-fun f67 () S42)
(declare-fun f68 (S43 S24) S6)
(declare-fun f69 (S44 S21) S43)
(declare-fun f70 () S44)
(declare-fun f71 (S45 S21) S6)
(declare-fun f72 (S46 S16) S45)
(declare-fun f73 () S46)
(declare-fun f74 (S47 S17) S6)
(declare-fun f75 (S48 S12) S47)
(declare-fun f76 () S48)
(declare-fun f77 () S6)
(declare-fun f78 (S49 S5) S10)
(declare-fun f79 () S49)
(declare-fun f80 (S50 S17) S18)
(declare-fun f81 () S50)
(declare-fun f82 (S51 S21) S22)
(declare-fun f83 () S51)
(declare-fun f84 (S52 S25) S26)
(declare-fun f85 () S52)
(declare-fun f86 (S53 S9) S29)
(declare-fun f87 () S53)
(declare-fun f88 (S54 S16) S31)
(declare-fun f89 () S54)
(declare-fun f90 (S55 S12) S33)
(declare-fun f91 () S55)
(declare-fun f92 (S56 S6) S1)
(declare-fun f93 (S6) S56)
(declare-fun f94 () S47)
(declare-fun f95 () S45)
(declare-fun f96 (S57 S25) S6)
(declare-fun f97 () S57)
(declare-fun f98 (S58 S9) S6)
(declare-fun f99 () S58)
(declare-fun f100 () S39)
(declare-fun f101 () S37)
(declare-fun f102 (S6 S6) S1)
(declare-fun f103 (S5 S5) S1)
(declare-fun f104 (S59 S6) S5)
(declare-fun f105 (S60 S5) S59)
(declare-fun f106 () S60)
(assert (not (= f1 f2)))
;(assert (forall ((?v0 S3)) (=> (= (f3 (f4 f5 f11) ?v0) f8) (= (f3 (f4 f5 f10) ?v0) f8))))
(assert (forall ((?v0 S3)) (= (f3 (f4 f5 f14) ?v0) f8)))
(assert (forall ((?v0 S2)) (= (= (f53 ?v0) f1) (forall ((?v1 S3) (?v2 S3)) (= (f3 ?v0 ?v1) (f3 ?v0 ?v2))))))
(check-sat)
(exit)
